Termination w.r.t. Q proof of TRS/Cimemaude2.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

GT₂(NzN, 0) -> U_4₁(is_NzNat₁(NzN))
U_3₃(True, NzN, NzM) -> GCD₂(d₂(NzN, NzM), NzM)
U_1₃(True, N, NzM) -> D₂(N, NzM)
U_11₃(True, N, NzM) -> U_1₃(gt₂(N, NzM), N, NzM)
U_21₃(True, NzM, N) -> GT₂(NzM, N)
D₂(s₁(N), s₁(M)) -> D₂(N, M)
*¹₂(s₁(N), s₁(M)) -> +¹₂(N, +₂(M, *₂(N, M)))
+¹₂(s₁(N), s₁(M)) -> +¹₂(N, M)
U_21₃(True, NzM, N) -> U_2₁(gt₂(NzM, N))
GCD₂(NzN, NzM) -> IS_NZNAT₁(NzM)
LT₂(N, M) -> GT₂(M, N)
GCD₂(NzN, NzM) -> IS_NZNAT₁(NzN)
QUOT₂(N, NzM) -> U_21₃(is_NzNat₁(NzM), NzM, N)
GCD₂(NzM, NzM) -> IS_NZNAT₁(NzM)
U_31₄(True, True, NzN, NzM) -> U_3₃(gt₂(NzN, NzM), NzN, NzM)
GT₂(s₁(N), s₁(M)) -> GT₂(N, M)
*¹₂(s₁(N), s₁(M)) -> *¹₂(N, M)
QUOT₂(N, NzM) -> U_11₃(is_NzNat₁(NzM), N, NzM)
GCD₂(NzN, NzM) -> U_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
QUOT₂(NzM, NzM) -> U_01₁(is_NzNat₁(NzM))
GCD₂(NzM, NzM) -> U_02₂(is_NzNat₁(NzM), NzM)
GT₂(NzN, 0) -> IS_NZNAT₁(NzN)
*¹₂(s₁(N), s₁(M)) -> +¹₂(M, *₂(N, M))
QUOT₂(NzM, NzM) -> IS_NZNAT₁(NzM)
U_3₃(True, NzN, NzM) -> D₂(NzN, NzM)
U_11₃(True, N, NzM) -> GT₂(N, NzM)
QUOT₂(N, NzM) -> IS_NZNAT₁(NzM)
U_31₄(True, True, NzN, NzM) -> GT₂(NzN, NzM)
U_1₃(True, N, NzM) -> QUOT₂(d₂(N, NzM), NzM)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

GT₂(NzN, 0) -> U_4₁(is_NzNat₁(NzN))
U_3₃(True, NzN, NzM) -> GCD₂(d₂(NzN, NzM), NzM)
U_1₃(True, N, NzM) -> D₂(N, NzM)
U_11₃(True, N, NzM) -> U_1₃(gt₂(N, NzM), N, NzM)
U_21₃(True, NzM, N) -> GT₂(NzM, N)
D₂(s₁(N), s₁(M)) -> D₂(N, M)
*¹₂(s₁(N), s₁(M)) -> +¹₂(N, +₂(M, *₂(N, M)))
+¹₂(s₁(N), s₁(M)) -> +¹₂(N, M)
U_21₃(True, NzM, N) -> U_2₁(gt₂(NzM, N))
GCD₂(NzN, NzM) -> IS_NZNAT₁(NzM)
LT₂(N, M) -> GT₂(M, N)
GCD₂(NzN, NzM) -> IS_NZNAT₁(NzN)
QUOT₂(N, NzM) -> U_21₃(is_NzNat₁(NzM), NzM, N)
GCD₂(NzM, NzM) -> IS_NZNAT₁(NzM)
U_31₄(True, True, NzN, NzM) -> U_3₃(gt₂(NzN, NzM), NzN, NzM)
GT₂(s₁(N), s₁(M)) -> GT₂(N, M)
*¹₂(s₁(N), s₁(M)) -> *¹₂(N, M)
QUOT₂(N, NzM) -> U_11₃(is_NzNat₁(NzM), N, NzM)
GCD₂(NzN, NzM) -> U_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
QUOT₂(NzM, NzM) -> U_01₁(is_NzNat₁(NzM))
GCD₂(NzM, NzM) -> U_02₂(is_NzNat₁(NzM), NzM)
GT₂(NzN, 0) -> IS_NZNAT₁(NzN)
*¹₂(s₁(N), s₁(M)) -> +¹₂(M, *₂(N, M))
QUOT₂(NzM, NzM) -> IS_NZNAT₁(NzM)
U_3₃(True, NzN, NzM) -> D₂(NzN, NzM)
U_11₃(True, N, NzM) -> GT₂(N, NzM)
QUOT₂(N, NzM) -> IS_NZNAT₁(NzM)
U_31₄(True, True, NzN, NzM) -> GT₂(NzN, NzM)
U_1₃(True, N, NzM) -> QUOT₂(d₂(N, NzM), NzM)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 6 SCCs with 19 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

D₂(s₁(N), s₁(M)) -> D₂(N, M)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

D₂(s₁(N), s₁(M)) -> D₂(N, M)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(D₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GT₂(s₁(N), s₁(M)) -> GT₂(N, M)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

GT₂(s₁(N), s₁(M)) -> GT₂(N, M)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(GT₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U_3₃(True, NzN, NzM) -> GCD₂(d₂(NzN, NzM), NzM)
U_31₄(True, True, NzN, NzM) -> U_3₃(gt₂(NzN, NzM), NzN, NzM)
GCD₂(NzN, NzM) -> U_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U_11₃(True, N, NzM) -> U_1₃(gt₂(N, NzM), N, NzM)
QUOT₂(N, NzM) -> U_11₃(is_NzNat₁(NzM), N, NzM)
U_1₃(True, N, NzM) -> QUOT₂(d₂(N, NzM), NzM)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

+¹₂(s₁(N), s₁(M)) -> +¹₂(N, M)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

+¹₂(s₁(N), s₁(M)) -> +¹₂(N, M)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(+¹₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

*¹₂(s₁(N), s₁(M)) -> *¹₂(N, M)

The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

*¹₂(s₁(N), s₁(M)) -> *¹₂(N, M)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(*¹₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s₁(x₁)) = 2 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

p₁(s₁(N)) -> N
+₂(N, 0) -> N
+₂(s₁(N), s₁(M)) -> s₁(s₁(+₂(N, M)))
*₂(N, 0) -> 0
*₂(s₁(N), s₁(M)) -> s₁(+₂(N, +₂(M, *₂(N, M))))
gt₂(0, M) -> False
gt₂(NzN, 0) -> u_4₁(is_NzNat₁(NzN))
u_4₁(True) -> True
is_NzNat₁(0) -> False
is_NzNat₁(s₁(N)) -> True
gt₂(s₁(N), s₁(M)) -> gt₂(N, M)
lt₂(N, M) -> gt₂(M, N)
d₂(0, N) -> N
d₂(s₁(N), s₁(M)) -> d₂(N, M)
quot₂(N, NzM) -> u_11₃(is_NzNat₁(NzM), N, NzM)
u_11₃(True, N, NzM) -> u_1₃(gt₂(N, NzM), N, NzM)
u_1₃(True, N, NzM) -> s₁(quot₂(d₂(N, NzM), NzM))
quot₂(NzM, NzM) -> u_01₁(is_NzNat₁(NzM))
u_01₁(True) -> s₁(0)
quot₂(N, NzM) -> u_21₃(is_NzNat₁(NzM), NzM, N)
u_21₃(True, NzM, N) -> u_2₁(gt₂(NzM, N))
u_2₁(True) -> 0
gcd₂(0, N) -> 0
gcd₂(NzM, NzM) -> u_02₂(is_NzNat₁(NzM), NzM)
u_02₂(True, NzM) -> NzM
gcd₂(NzN, NzM) -> u_31₄(is_NzNat₁(NzN), is_NzNat₁(NzM), NzN, NzM)
u_31₄(True, True, NzN, NzM) -> u_3₃(gt₂(NzN, NzM), NzN, NzM)
u_3₃(True, NzN, NzM) -> gcd₂(d₂(NzN, NzM), NzM)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.